1 /-
2 Copyright (c) 2019 Johannes Hölzl, Zhouhang Zhou. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Zhouhang Zhou
5 -/
6
7 import measure_theory.integration
src └────────────────────────┘
8
9 /-!
10
11 # Almost everywhere equal functions
12
13 Two measurable functions are treated as identical if they are almost everywhere equal. We form the
14 set of equivalence classes under the relation of being almost everywhere equal, which is sometimes
15 known as the `L⁰` space.
16
17 See `l1_space.lean` for `L¹` space.
18
19
20 ## Notation
21
22 * `α →ₘ β` is the type of `L⁰` space, where `α` is a measure space and `β` is a measurable space.
23 `f : α →ₘ β` is a "function" in `L⁰`. In comments, `[f]` is also used to denote an `L⁰` function.
24
25 `ₘ` can be typed as `\_m`. Sometimes it is shown as a box if font is missing.
26
27
28 ## Main statements
29
30 * The linear structure of `L⁰` :
31 Addition and scalar multiplication are defined on `L⁰` in the natural way, i.e.,
32 `[f] + [g] := [f + g]`, `c • [f] := [c • f]`. So defined, `α →ₘ β` inherits the linear structure
33 of `β`. For example, if `β` is a module, then `α →ₘ β` is a module over the same ring.
34
35 See `mk_add_mk`, `neg_mk`, `mk_sub_mk`, `smul_mk`,
36 `add_to_fun`, `neg_to_fun`, `sub_to_fun`, `smul_to_fun`
37
38 * The order structure of `L⁰` :
39 `≤` can be defined in a similar way: `[f] ≤ [g]` if `f a ≤ g a` for almost all `a` in domain.
40 And `α →ₘ β` inherits the preorder and partial order of `β`.
41
42 TODO: Define `sup` and `inf` on `L⁰` so that it forms a lattice. It seems that `β` must be a
43 linear order, since otherwise `f ⊔ g` may not be a measurable function.
44
45 * Emetric on `L⁰` :
46 If `β` is an `emetric_space`, then `L⁰` can be made into an `emetric_space`, where
47 `edist [f] [g]` is defined to be `∫⁻ a, edist (f a) (g a)`.
48
49 The integral used here is `lintegral : (α → ennreal) → ennreal`, which is defined in the file
50 `integration.lean`.
51
52 See `edist_mk_mk` and `edist_to_fun`.
53
54
55 ## Implementation notes
56
57 * `f.to_fun` : To find a representative of `f : α →ₘ β`, use `f.to_fun`.
58 For each operation `op` in `L⁰`, there is a lemma called `op_to_fun`, characterizing,
59 say, `(f op g).to_fun`.
60 * `ae_eq_fun.mk` : To constructs an `L⁰` function `α →ₘ β` from a measurable function `f : α → β`,
61 use `ae_eq_fun.mk`
62 * `comp` : Use `comp g f` to get `[g ∘ f]` from `g : β → γ` and `[f] : α →ₘ γ`
63 * `comp₂` : Use `comp₂ g f₁ f₂ to get `[λa, g (f₁ a) (f₂ a)]`.
64 For example, `[f + g]` is `comp₂ (+)`
65
66
67 ## Tags
68
69 function space, almost everywhere equal, `L⁰`, ae_eq_fun
70
71 -/
72
73 noncomputable theory
74 open_locale classical
75
76 namespace measure_theory
77 open set lattice filter topological_space
78
79 universes u v
80 variables {α : Type u} {β : Type v} [measure_space α]
id └───────────┘
src └───────────┘
typ └───────────┘
doc └───────────┘
81
82 section measurable_space
83 variables [measurable_space β]
id └──────────────┘
src └──────────────┘
typ └──────────────┘
84
85 variables (α β)
86
87 /-- The equivalence relation of being almost everywhere equal -/
88 instance ae_eq_fun.setoid : setoid { f : α → β // measurable f } :=
id └────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
src └────┘ ┴ └────────┘
typ └────┘ ┴ ┴ ┴ ┴ └────────┘ ┴
doc └────────┘
89 ⟨ λf g, ∀ₘ a, f.1 a = g.1 a,
id ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴
src └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └┘ ┴┴ ┴┴ ┴ ┴ ┴┴ ┴
doc └┘ ┴
90 assume ⟨f, hf⟩, by filter_upwards [] assume a, rfl,
id ┴ └─┘
src └────────────────┘ └──┘└─┘
typ ┴ └────────────────┘ └──┘└─┘
doc └────────────────┘ └──┘
txt └────────────────┘ └──┘
par └────────────────┘ └──┘
pid └─┘┴ └──┘
st └──────────────────────────────┘
91 assume ⟨f, hf⟩ ⟨g, hg⟩ hfg, by filter_upwards [hfg] assume a, eq.symm,
id ┴ ┴ └─┘ └─────┘
src └──────────────┘ └┘ └──┘└─────┘
typ ┴ ┴ └─┘ └──────────────┘ └┘ └──┘└─────┘
doc └──────────────┘ └┘ └──┘
txt └──────────────┘ └┘ └──┘
par └──────────────┘ └┘ └──┘
pid └┘ ┴┴ └──┘
st └─────────────────────────────────────┘
92 assume ⟨f, hf⟩ ⟨g, hg⟩ ⟨h, hh⟩ hfg hgh, by filter_upwards [hfg, hgh] assume a, eq.trans ⟩
id ┴ ┴ ┴ └─┘ └─┘ └──────┘
src └──────────────┘ └┘ └┘ └──┘└──────┘┴
typ ┴ ┴ ┴ └─┘ └─┘ └──────────────┘ └┘ └┘ └──┘└──────┘┴
doc └──────────────┘ └┘ └┘ └──┘ ┴
txt └──────────────┘ └┘ └┘ └──┘ ┴
par └──────────────┘ └┘ └┘ └──┘ ┴
pid └┘ └┘ ┴┴ └──┘ ┴
st └────────────────────────────────────────────┘
93
94 /-- The space of equivalence classes of measurable functions, where two measurable functions are
95 equivalent if they agree almost everywhere, i.e., they differ on a set of measure `0`. -/
96 def ae_eq_fun : Type (max u v) := quotient (ae_eq_fun.setoid α β)
id └──────┘ └──────────────┘ ┴ ┴
src └──────┘ └──────────────┘
typ └──────┘ └──────────────┘ ┴ ┴
doc └──────────────┘
97
98 variables {α β}
99
100 infixr ` →ₘ `:25 := ae_eq_fun
id └───────┘
src └───────┘
typ └───────┘
doc └───────┘
101
102 end measurable_space
103
104 namespace ae_eq_fun
105 variables [measurable_space β]
id └──────────────┘
src └──────────────┘
typ └──────────────┘
106
107 /-- Construct the equivalence class `[f]` of a measurable function `f`, based on the equivalence
108 relation of being almost everywhere equal. -/
109 def mk (f : α → β) (hf : measurable f) : α →ₘ β := quotient.mk ⟨f, hf⟩
id ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ └─────────┘ ┴ └┘
src └────────┘ └┘ └─────────┘
typ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ └─────────┘ ┴ └┘
doc └────────┘ └┘
110
111 /-- A representative of an `ae_eq_fun` [f] -/
112 protected def to_fun (f : α →ₘ β) : α → β := @quotient.out _ (ae_eq_fun.setoid α β) f
id ┴ └┘ ┴ ┴ ┴ └──────────┘ └──────────────┘ ┴ ┴ ┴
src └┘ └──────────┘ └──────────────┘
typ ┴ └┘ ┴ ┴ ┴ └──────────┘ └──────────────┘ ┴ ┴ ┴
doc └┘ └──────────┘ └──────────────┘
113
114 protected lemma measurable (f : α →ₘ β) : measurable f.to_fun :=
id ┴ └┘ ┴ └────────┘ ┴└─────┘
src └┘ └────────┘ └─────┘
typ ┴ └┘ ┴ └────────┘ ┴└─────┘
doc └┘ └────────┘ └─────┘
115 (@quotient.out _ (ae_eq_fun.setoid α β) f).2
id └──────────┘ └──────────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └──────────────┘ ┴
typ └──────────┘ └──────────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └──────────────┘
116
117 instance : has_coe (α →ₘ β) (α → β) := ⟨λf, f.to_fun⟩
id └─────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴└─────┘
src └─────┘ └┘ └─────┘
typ └─────┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴└─────┘
doc └┘ └─────┘
118
119 @[simp] lemma quot_mk_eq_mk (f : {f : α → β // measurable f}) : quot.mk setoid.r f = mk f.1 f.2 :=
id ┴ ┴ ┴ ┴ └────────┘ ┴ └─────┘ └──────┘ ┴ ┴ └┘ ┴┴ ┴┴
src ┴ └────────┘ └──────┘ ┴ └┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └────────┘ ┴ └─────┘ └──────┘ ┴ ┴ └┘ ┴┴ ┴┴
doc └──┘ └────────┘ └┘
120 by cases f; refl
id ┴
src └────┘ └────
typ └────┘┴ └────
doc └────┘ └────
txt └────┘ └────
par └────┘ └────
pid ┴ └
st └──────────────
121
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
122 @[simp] lemma mk_eq_mk (f g : α → β) (hf hg) :
id ┴ ┴
typ ┴ ┴
doc └──┘
123 mk f hf = mk g hg ↔ (∀ₘ a, f a = g a) :=
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘ ┴
124 ⟨quotient.exact, assume h, quotient.sound h⟩
id └────────────┘ ┴ └────────────┘ ┴
src └────────────┘ └────────────┘
typ └────────────┘ ┴ └────────────┘ ┴
125
126 @[ext] lemma ext (f g : α →ₘ β) (f' g' : α → β) (hf' hg') (hf : mk f' hf' = f)
id ┴ └┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ ┴
src └┘ └┘ ┴
typ ┴ └┘ ┴ ┴ ┴ └┘ └┘ └─┘ ┴ ┴
doc └─┘ └┘ └┘
127 (hg : mk g' hg' = g) (h : ∀ₘ a, f' a = g' a) : f = g :=
id └┘ └┘ └─┘ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ ┴ ┴ ┴
typ └┘ └┘ └─┘ ┴ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └┘ └┘ ┴
128 by { rw [← hf, ← hg], rw mk_eq_mk, assumption }
id └┘ └┘ └──────┘
src └────┘ └──┘ ┴ └─┘└──────┘ └─────────┘
typ └────┘└┘└──┘└┘┴ └─┘└──────┘ └─────────┘
doc └────┘ └──┘ ┴ └─┘ └─────────┘
txt └────┘ └──┘ ┴ └─┘ └─────────┘
par └────┘ └──┘ ┴ └─┘ └─────────┘
pid └──┘ └──┘ ┴ ┴ ┴
st └─────────┘└────┘└────────────┘└───────────┘└┘
129
130 lemma self_eq_mk (f : α →ₘ β) : f = mk (f.to_fun) f.measurable :=
id ┴ └┘ ┴ ┴ ┴ └┘ ┴└─────┘ ┴└─────────┘
src └┘ ┴ └┘ └─────┘ └─────────┘
typ ┴ └┘ ┴ ┴ ┴ └┘ ┴└─────┘ ┴└─────────┘
doc └┘ └┘ └─────┘
131 by simp [mk, ae_eq_fun.to_fun]
id └┘ └──────────────┘
src └────┘└┘└┘└──────────────┘└─
typ └────┘└┘└┘└──────────────┘└─
doc └────┘└┘└┘└──────────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────
132
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
133 lemma all_ae_mk_to_fun (f : α → β) (hf) : ∀ₘ a, (mk f hf).to_fun a = f a :=
id ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴
src └┘ ┴ └┘ └────┘ ┴
typ ┴ ┴ └┘ ┴┴ └┘ ┴ └┘ └────┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └┘ └────┘
134 by rw [← mk_eq_mk _ f _ hf, ← self_eq_mk (mk f hf)]
id └──────┘ ┴ └┘ └────────┘ └┘ ┴ └┘
src └────┘└──────┘└─┘ └─┘ └──┘└────────┘┴ └┘┴ ┴ └──
typ └────┘└──────┘└─┘┴└─┘└┘└──┘└────────┘┴ └┘┴┴┴└┘└──
doc └────┘ └─┘ └─┘ └──┘ ┴ └┘┴ ┴ └──
txt └────┘ └─┘ └─┘ └──┘ ┴ ┴ ┴ └──
par └────┘ └─┘ └─┘ └──┘ ┴ ┴ ┴ └──
pid └──┘ └─┘ └─┘ └──┘ ┴ ┴ ┴ └┘└
st └──────────────────────┘└──────────────────────┘┴└
135
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
136 /-- Given a measurable function `g : β → γ`, and an almost everywhere equal function `[f] : α →ₘ β`,
137 return the equivalence class of `g ∘ f`, i.e., the almost everywhere equal function
138 `[g ∘ f] : α →ₘ γ`. -/
139 def comp {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) : α →ₘ γ :=
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └──────────────┘ └────────┘ └┘ └┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘ └┘
140 quotient.lift_on f (λf, mk (g ∘ f.1) (measurable.comp hg f.2)) $ assume f₁ f₂ eq,
id └──────────────┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─────────────┘ └┘ ┴┴ └┘ └┘ └┘
src └──────────────┘ └┘ ┴ ┴ └─────────────┘ ┴ └┘
typ └──────────────┘ ┴ ┴ └┘ ┴ ┴ ┴┴ └─────────────┘ └┘ ┴┴ └┘ └┘ └┘
doc └┘
141 by refine quotient.sound _; filter_upwards [eq] assume a, congr_arg g
id └────────────┘ └───────┘ ┴
src └─────┘└────────────┘└┘ └──────────────┘ └┘ └──┘└───────┘┴ └
typ └─────┘└────────────┘└┘ └──────────────┘ └┘ └──┘└───────┘┴┴└
doc └─────┘ └┘ └──────────────┘ └┘ └──┘ ┴ └
txt └─────┘ └┘ └──────────────┘ └┘ └──┘ ┴ └
par └─────┘ └┘ └──────────────┘ └┘ └──┘ ┴ └
pid ┴ └┘ └┘ ┴┴ └──┘ ┴ └
st └───────────────────────────────────────────────────────────────────
142
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
143 @[simp] lemma comp_mk {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g)
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └──────────────┘ └────────┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └──┘ └────────┘
144 (f : α → β) (hf) : comp g hg (mk f hf) = mk (g ∘ f) (measurable.comp hg hf) :=
id ┴ ┴ └──┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────────────┘ └┘ └┘
src └──┘ └┘ ┴ └┘ ┴ └─────────────┘
typ ┴ ┴ └──┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────────────┘ └┘ └┘
doc └──┘ └┘ └┘
145 rfl
id └─┘
src └─┘
typ └─┘
146
147 lemma comp_eq_mk_to_fun {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
src └──────────────┘ └────────┘ └┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘
148 comp g hg f = mk (g ∘ f.to_fun) (hg.comp f.measurable) :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└─────┘ └┘└───┘ ┴└─────────┘
src └──┘ ┴ └┘ ┴ └─────┘ └───┘ └─────────┘
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴└─────┘ └┘└───┘ ┴└─────────┘
doc └──┘ └┘ └─────┘
149 by conv_lhs { rw [self_eq_mk f, comp_mk] }
id └────────┘ ┴ └─────┘
src └─────────┘└──┘└────────┘┴ └┘└─────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└─────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└───────┘ ┴┴└
150
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
151 lemma comp_to_fun {γ : Type*} [measurable_space γ] (g : β → γ) (hg : measurable g) (f : α →ₘ β) :
id └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
src └──────────────┘ └────────┘ └┘
typ └──────────────┘ ┴ ┴ ┴ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘
152 ∀ₘ a, (comp g hg f).to_fun a = (g ∘ f.to_fun) a :=
id └┘ ┴┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
src └┘ ┴ └──┘ └────┘ ┴ ┴ └─────┘
typ └┘ ┴┴ └──┘ ┴ └┘ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
doc └┘ ┴ └──┘ └────┘ └─────┘
153 by { rw comp_eq_mk_to_fun, apply all_ae_mk_to_fun }
id └───────────────┘ └──────────────┘
src └─┘└───────────────┘ └────┘└──────────────┘┴
typ └─┘└───────────────┘ └────┘└──────────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └─────────────────────┘└───────────────────────┘└┘
154
155 /-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
156 `[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
157 `λa, g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
158 `[λa, g (f₁ a) (f₂ a)] : α →ₘ γ` -/
159 def comp₂ {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
160 (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) : α →ₘ δ :=
id ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────┘ ┴ ┴ ┴ └┘ └┘ └┘
typ ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘ └┘ └┘
161 begin
st └─────
162 refine quotient.lift_on₂ f₁ f₂ (λf₁ f₂, mk (λa, g (f₁.1 a) (f₂.1 a)) $ _) _,
id └───────────────┘ └┘ └┘ └┘ ┴
src └─────┘└───────────────┘┴ ┴ ┴ └─────┘└┘┴ └─┘ ┴ └─┘ └┘ └─┘ └─┘ └───┘
typ └─────┘└───────────────┘┴└┘┴└┘┴ └─────┘└┘┴ └─┘┴┴ └─┘ └┘ └─┘ └─┘ └───┘
doc └─────┘ ┴ ┴ ┴ └─────┘└┘┴ └─┘ ┴ └─┘ └┘ └─┘ └─┘ └───┘
txt └─────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ └─┘ └┘ └─┘ └─┘ └───┘
par └─────┘ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ └─┘ └┘ └─┘ └─┘ └───┘
pid ┴ ┴ ┴ ┴ └─────┘ ┴ └─┘ ┴ └─┘ └┘ └─┘ └─┘ └───┘
st ────────────────────────────────────────────────────────────────────────────┘└─
163 { exact measurable.comp hg (measurable.prod_mk f₁.2 f₂.2) },
id └─────────────┘ └┘ └────────────────┘ └┘ └┘
src └────┘└─────────────┘┴ ┴ └────────────────┘┴ └─┘ └──┘
typ └────┘└─────────────┘┴└┘┴ └────────────────┘┴└┘└─┘└┘└──┘
doc └────┘ ┴ ┴ ┴ └─┘ └──┘
txt └────┘ ┴ ┴ ┴ └─┘ └──┘
par └────┘ ┴ ┴ ┴ └─┘ └──┘
pid ┴ ┴ ┴ ┴ └─┘ └─┘┴
st ───┘└──────────────────────────────────────────────────────┘└┘└
164 { rintros ⟨f₁, hf₁⟩ ⟨f₂, hf₂⟩ ⟨g₁, hg₁⟩ ⟨g₂, hg₂⟩ h₁ h₂,
src └───────────────────────────────────────────────────┘
typ └───────────────────────────────────────────────────┘
doc └───────────────────────────────────────────────────┘
txt └───────────────────────────────────────────────────┘
par └───────────────────────────────────────────────────┘
pid └────────────────────────────────────────────┘
st ────────────────────────────────────────────────────────┘└─
165 refine quotient.sound _,
id └────────────┘
src └─────┘└────────────┘└┘
typ └─────┘└────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ──────────────────────────┘└─
166 filter_upwards [h₁, h₂],
src └──────────────┘ └┘ ┴
typ └──────────────┘ └┘ ┴
doc └──────────────┘ └┘ ┴
txt └──────────────┘ └┘ ┴
par └──────────────┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────┘└─
167 simp {contextual := tt} }
id └┘
src └───┘ └────────────┘└┘└┘
typ └───┘ └────────────┘└┘└┘
doc └───┘ └────────────┘ └┘
txt └───┘ └────────────┘ └┘
par └───┘ └────────────┘ └┘
pid ┴ └────────────┘ ┴┴
st ───────────────────────────┘└─
168 end
st ──┘
169
170 @[simp] lemma comp₂_mk_mk {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
doc └──┘
171 (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α → β) (f₂ : α → γ) (hf₁ hf₂) :
id ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴
typ ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
doc └────────┘
172 comp₂ g hg (mk f₁ hf₁) (mk f₂ hf₂) =
id └───┘ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ └─┘ ┴
src └───┘ └┘ └┘ ┴
typ └───┘ ┴ └┘ └┘ └┘ └─┘ └┘ └┘ └─┘ ┴
doc └───┘ └┘ └┘
173 mk (λa, g (f₁ a) (f₂ a)) (measurable.comp hg (measurable.prod_mk hf₁ hf₂)) :=
id └┘ ┴ ┴ └┘ ┴ └┘ ┴ └─────────────┘ └┘ └────────────────┘ └─┘ └─┘
src └┘ └─────────────┘ └────────────────┘
typ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └─────────────┘ └┘ └────────────────┘ └─┘ └─┘
doc └┘
174 rfl
id └─┘
src └─┘
typ └─┘
175
176 lemma comp₂_eq_mk_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
177 (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) :
id ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────┘ ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘ └┘
178 comp₂ g hg f₁ f₂ = mk (λa, g (f₁.to_fun a) (f₂.to_fun a))
id └───┘ ┴ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴
src └───┘ ┴ └┘ └─────┘ └─────┘
typ └───┘ ┴ └┘ └┘ └┘ ┴ └┘ ┴ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴
doc └───┘ └┘ └─────┘ └─────┘
179 (hg.comp (measurable.prod_mk f₁.measurable f₂.measurable)) :=
id └┘└───┘ └────────────────┘ └┘└─────────┘ └┘└─────────┘
src └───┘ └────────────────┘ └─────────┘ └─────────┘
typ └┘└───┘ └────────────────┘ └┘└─────────┘ └┘└─────────┘
180 by conv_lhs { rw [self_eq_mk f₁, self_eq_mk f₂, comp₂_mk_mk] }
id └────────┘ └┘ └────────┘ └┘ └─────────┘
src └─────────┘└──┘└────────┘┴ └┘└────────┘┴ └┘└─────────┘└┘└─
typ └─────────┘└──┘└────────┘┴└┘└┘└────────┘┴└┘└┘└─────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ ┴ └┘ └─┘└
st └─────────┘└────────────────┘└─────────────┘└───────────┘ ┴┴└
181
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
182 lemma comp₂_to_fun {γ δ : Type*} [measurable_space γ] [measurable_space δ]
id └──────────────┘ ┴ └──────────────┘ ┴
src └──────────────┘ └──────────────┘
typ └──────────────┘ ┴ └──────────────┘ ┴
183 (g : β → γ → δ) (hg : measurable (λp:β×γ, g p.1 p.2)) (f₁ : α →ₘ β) (f₂ : α →ₘ γ) :
id ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────────┘ ┴ ┴ ┴ └┘ └┘
typ ┴ ┴ ┴ └────────┘ ┴┴┴ ┴ ┴┴ ┴┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘ └┘
184 ∀ₘ a, (comp₂ g hg f₁ f₂).to_fun a = g (f₁.to_fun a) (f₂.to_fun a) :=
id └┘ ┴┴ └───┘ ┴ └┘ └┘ └┘ └────┘ ┴ ┴ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴
src └┘ ┴ └───┘ └────┘ ┴ └─────┘ └─────┘
typ └┘ ┴┴ └───┘ ┴ └┘ └┘ └┘ └────┘ ┴ ┴ ┴ └┘└─────┘ ┴ └┘└─────┘ ┴
doc └┘ ┴ └───┘ └────┘ └─────┘ └─────┘
185 by { rw comp₂_eq_mk_to_fun, apply all_ae_mk_to_fun }
id └────────────────┘ └──────────────┘
src └─┘└────────────────┘ └────┘└──────────────┘┴
typ └─┘└────────────────┘ └────┘└──────────────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └──────────────────────┘└───────────────────────┘└┘
186
187 /-- Given a predicate `p` and an equivalence class `[f]`, return true if `p` holds of `f a`
188 for almost all `a` -/
189 def lift_pred (p : β → Prop) (f : α →ₘ β) : Prop :=
id ┴ ┴ └┘ ┴
src └┘
typ ┴ ┴ └┘ ┴
doc └┘
190 quotient.lift_on f (λf, ∀ₘ a, p (f.1 a))
id └──────────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴┴ ┴
src └──────────────┘ └┘ ┴ ┴
typ └──────────────┘ ┴ ┴ └┘ ┴┴ ┴ ┴┴ ┴
doc └┘ ┴
191 begin
st └─────
192 assume f g h, dsimp, refine propext (all_ae_congr _),
id └─────┘ └──────────┘
src └──────────┘ └───┘ └─────┘└─────┘┴ └──────────┘└─┘
typ └──────────┘ └───┘ └─────┘└─────┘┴ └──────────┘└─┘
doc └──────────┘ └───┘ └─────┘ ┴ └─┘
txt └──────────┘ └───┘ └─────┘ ┴ └─┘
par └──────────┘ └───┘ └─────┘ ┴ └─┘
pid └──────────┘ ┴ ┴ └─┘
st ─────────────┘└─────┘└───────────────────────────────┘└─
193 filter_upwards [h], simp {contextual := tt}
id └┘
src └──────────────┘ ┴ └───┘ └────────────┘└┘└┘
typ └──────────────┘ ┴ └───┘ └────────────┘└┘└┘
doc └──────────────┘ ┴ └───┘ └────────────┘ └┘
txt └──────────────┘ ┴ └───┘ └────────────┘ └┘
par └──────────────┘ ┴ └───┘ └────────────┘ └┘
pid └┘ ┴ ┴ └────────────┘ ┴┴
st ───────────────────┘└────────────────────────┘
194 end
st └─┘
195
196 /-- Given a relation `r` and equivalence class `[f]` and `[g]`, return true if `r` holds of
197 `(f a, g a)` for almost all `a` -/
198 def lift_rel {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β) (g : α →ₘ γ) : Prop :=
id └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └──────────────┘ └┘ └┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
199 lift_pred (λp:β×γ, r p.1 p.2)
id └───────┘ ┴┴┴ ┴ ┴┴ ┴┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴┴┴ ┴ ┴┴ ┴┴
doc └───────┘
200 (comp₂ prod.mk (measurable.prod_mk
id └───┘ └─────┘ └────────────────┘
src └───┘ └─────┘ └────────────────┘
typ └───┘ └─────┘ └────────────────┘
doc └───┘
201 (measurable.fst measurable_id) (measurable.snd measurable_id)) f g)
id └────────────┘ └───────────┘ └────────────┘ └───────────┘ ┴ ┴
src └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └────────────┘ └───────────┘ └────────────┘ └───────────┘ ┴ ┴
202
203 lemma lift_rel_mk_mk {γ : Type*} [measurable_space γ] (r : β → γ → Prop)
id └──────────────┘ ┴ ┴ ┴
src └──────────────┘
typ └──────────────┘ ┴ ┴ ┴
204 (f : α → β) (g : α → γ) (hf hg) : lift_rel r (mk f hf) (mk g hg) ↔ ∀ₘ a, r (f a) (g a) :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └┘ └┘ ┴ └┘ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └──────┘ └┘ └┘ └┘ ┴
205 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
206
207 lemma lift_rel_iff_to_fun {γ : Type*} [measurable_space γ] (r : β → γ → Prop) (f : α →ₘ β)
id └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └──────────────┘ └┘
typ └──────────────┘ ┴ ┴ ┴ ┴ └┘ ┴
doc └┘
208 (g : α →ₘ γ) : lift_rel r f g ↔ ∀ₘ a, r (f.to_fun a) (g.to_fun a) :=
id ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴└─────┘ ┴ ┴└─────┘ ┴
src └┘ └──────┘ ┴ └┘ ┴ └─────┘ └─────┘
typ ┴ └┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴ ┴└─────┘ ┴ ┴└─────┘ ┴
doc └┘ └──────┘ └┘ ┴ └─────┘ └─────┘
209 by conv_lhs { rw [self_eq_mk f, self_eq_mk g, lift_rel_mk_mk] }
id └────────┘ ┴ └────────┘ ┴ └────────────┘
src └─────────┘└──┘└────────┘┴ └┘└────────┘┴ └┘└────────────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└────────┘┴┴└┘└────────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└────────────┘└──────────────┘ ┴┴└
210
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
211 section order
212
213 instance [preorder β] : preorder (α →ₘ β) :=
id └──────┘ ┴ └──────┘ ┴ └┘ ┴
src └──────┘ └──────┘ └┘
typ └──────┘ ┴ └──────┘ ┴ └┘ ┴
doc └┘
214 { le := lift_rel (≤),
id ┴ └──────┘ ┴
src ┴ └──────┘ ┴
typ ┴ └──────┘ ┴
doc └──────┘
215 le_refl := by rintros ⟨⟨f, hf⟩⟩; exact univ_mem_sets' (assume a, le_refl _),
id └────────────┘ └─────┘
src └───────────────┘ └────┘└────────────┘┴ └──┘└─────┘└─┘
typ └───────────────┘ └────┘└────────────┘┴ └──┘└─────┘└─┘
doc └───────────────┘ └────┘ ┴ └──┘ └─┘
txt └───────────────┘ └────┘ ┴ └──┘ └─┘
par └───────────────┘ └────┘ ┴ └──┘ └─┘
pid └────────┘ ┴ ┴ └──┘ └─┘
st └────────────────────────────────────────────────────────────┘
216 le_trans :=
217 begin
st └─────
218 rintros ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩ ⟨⟨h, hh⟩⟩ hfg hgh,
src └───────────────────────────────────────────┘
typ └───────────────────────────────────────────┘
doc └───────────────────────────────────────────┘
txt └───────────────────────────────────────────┘
par └───────────────────────────────────────────┘
pid └────────────────────────────────────┘
st ────────────────────────────────────────────────┘└─
219 filter_upwards [hfg, hgh] assume a, le_trans
id └──────┘
src └──────────────┘ └┘ └┘ └──┘└──────┘└
typ └──────────────┘ └┘ └┘ └──┘└──────┘└
doc └──────────────┘ └┘ └┘ └──┘ └
txt └──────────────┘ └┘ └┘ └──┘ └
par └──────────────┘ └┘ └┘ └──┘ └
pid └┘ └┘ ┴┴ └──┘ └
st ─────────────────────────────────────────────────
220 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
221
222 lemma mk_le_mk [preorder β] {f g : α → β} (hf hg) : mk f hf ≤ mk g hg ↔ ∀ₘ a, f a ≤ g a :=
id └──────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘ ┴
223 iff.rfl
id └─────┘
src └─────┘
typ └─────┘
224
225 lemma le_iff_to_fun_le [preorder β] {f g : α →ₘ β} : f ≤ g ↔ ∀ₘ a, f.to_fun a ≤ g.to_fun a :=
id └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └──────┘ └┘ ┴ ┴ └┘ ┴ └─────┘ ┴ └─────┘
typ └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └─────┘ └─────┘
226 by { conv_lhs { rw [self_eq_mk f, self_eq_mk g] }, rw mk_le_mk }
id └────────┘ ┴ └────────┘ ┴ └──────┘
src └─────────┘└──┘└────────┘┴ └┘└────────┘┴ └┘┴ └─┘└──────┘┴
typ └─────────┘└──┘└────────┘┴┴└┘└────────┘┴┴└┘┴ └─┘└──────┘┴
doc └─┘ ┴
txt └─────────┘└──┘ ┴ └┘ ┴ └┘┴ └─┘ ┴
par └─────────┘└──┘ ┴ └┘ ┴ └┘┴ └─┘ ┴
pid ┴└────┘ ┴ └┘ ┴ └─┘ ┴ ┴
st └───────────┘└───────────────┘└────────────┘ ┴└┘└───────────┘└┘
227
228 instance [partial_order β] : partial_order (α →ₘ β) :=
id └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
src └───────────┘ └───────────┘ └┘
typ └───────────┘ ┴ └───────────┘ ┴ └┘ ┴
doc └┘
229 { le_antisymm :=
230 begin
st └─────
231 rintros ⟨⟨f, hf⟩⟩ ⟨⟨g, hg⟩⟩ hfg hgf,
src └─────────────────────────────────┘
typ └─────────────────────────────────┘
doc └─────────────────────────────────┘
txt └─────────────────────────────────┘
par └─────────────────────────────────┘
pid └──────────────────────────┘
st ──────────────────────────────────────┘└─
232 refine quotient.sound _,
id └────────────┘
src └─────┘└────────────┘└┘
typ └─────┘└────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ──────────────────────────┘└─
233 filter_upwards [hfg, hgf] assume a, le_antisymm
id └─────────┘
src └──────────────┘ └┘ └┘ └──┘└─────────┘└
typ └──────────────┘ └┘ └┘ └──┘└─────────┘└
doc └──────────────┘ └┘ └┘ └──┘ └
txt └──────────────┘ └┘ └┘ └──┘ └
par └──────────────┘ └┘ └┘ └──┘ └
pid └┘ └┘ ┴┴ └──┘ └
st ────────────────────────────────────────────────────
234 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
235 .. ae_eq_fun.preorder }
id └────────────────┘
src └────────────────┘
typ └────────────────┘
236
237 /- TODO: Prove `L⁰` space is a lattice if β is linear order.
238 What if β is only a lattice? -/
239
240 -- instance [linear_order β] : semilattice_sup (α →ₘ β) :=
241 -- { sup := comp₂ (⊔) (_),
242 -- .. ae_eq_fun.partial_order }
243
244 end order
245
246 variable (α)
247 /-- The equivalence class of a constant function: `[λa:α, b]`, based on the equivalence relation of
248 being almost everywhere equal -/
249 def const (b : β) : α →ₘ β := mk (λa:α, b) measurable_const
id ┴ ┴ └┘ ┴ └┘ ┴ ┴ └──────────────┘
src └┘ └┘ └──────────────┘
typ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └──────────────┘
doc └┘ └┘
250
251 lemma const_to_fun (b : β) : ∀ₘ a, (const α b).to_fun a = b := all_ae_mk_to_fun _ _
id ┴ └┘ ┴┴ └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ └──────────────┘
src └┘ ┴ └───┘ └────┘ ┴ └──────────────┘
typ ┴ └┘ ┴┴ └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ └──────────────┘
doc └┘ ┴ └───┘ └────┘
252 variable {α}
253
254 instance [inhabited β] : inhabited (α →ₘ β) := ⟨const _ (default _)⟩
id └───────┘ ┴ └───────┘ ┴ └┘ ┴ └───┘ └─────┘
src └───────┘ └───────┘ └┘ └───┘ └─────┘
typ └───────┘ ┴ └───────┘ ┴ └┘ ┴ └───┘ └─────┘
doc └┘ └───┘
255
256 instance [has_zero β] : has_zero (α →ₘ β) := ⟨const α 0⟩
id └──────┘ ┴ └──────┘ ┴ └┘ ┴ └───┘ ┴
src └──────┘ └──────┘ └┘ └───┘
typ └──────┘ ┴ └──────┘ ┴ └┘ ┴ └───┘ ┴
doc └┘ └───┘
257 lemma zero_def [has_zero β] : (0 : α →ₘ β) = mk (λa:α, 0) measurable_const := rfl
id └──────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────────────┘ └─┘
src └──────┘ └┘ ┴ └┘ └──────────────┘ └─┘
typ └──────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────────────┘ └─┘
doc └┘ └┘
258 lemma zero_to_fun [has_zero β] : ∀ₘ a, (0 : α →ₘ β).to_fun a = 0 := const_to_fun _ _
id └──────┘ ┴ └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──────────┘
src └──────┘ └┘ ┴ └┘ └────┘ ┴ └──────────┘
typ └──────┘ ┴ └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──────────┘
doc └┘ ┴ └┘ └────┘
259
260 instance [has_one β] : has_one (α →ₘ β) := ⟨const α 1⟩
id └─────┘ ┴ └─────┘ ┴ └┘ ┴ └───┘ ┴
src └─────┘ └─────┘ └┘ └───┘
typ └─────┘ ┴ └─────┘ ┴ └┘ ┴ └───┘ ┴
doc └┘ └───┘
261 lemma one_def [has_one β] : (1 : α →ₘ β) = mk (λa:α, 1) measurable_const := rfl
id └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────────────┘ └─┘
src └─────┘ └┘ ┴ └┘ └──────────────┘ └─┘
typ └─────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ └──────────────┘ └─┘
doc └┘ └┘
262 lemma one_to_fun [has_one β] : ∀ₘ a, (1 : α →ₘ β).to_fun a = 1 := const_to_fun _ _
id └─────┘ ┴ └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──────────┘
src └─────┘ └┘ ┴ └┘ └────┘ ┴ └──────────┘
typ └─────┘ ┴ └┘ ┴┴ ┴ └┘ ┴ └────┘ ┴ ┴ └──────────┘
doc └┘ ┴ └┘ └────┘
263
264 section add_monoid
265 variables {γ : Type*}
266 [topological_space γ] [second_countable_topology γ] [add_monoid γ] [topological_add_monoid γ]
id └───────────────┘ └───────────────────────┘ └────────┘ └────────────────────┘
src └───────────────┘ └───────────────────────┘ └────────┘ └────────────────────┘
typ └───────────────┘ └───────────────────────┘ └────────┘ └────────────────────┘
doc └───────────────┘ └───────────────────────┘ └────────────────────┘
267
268 protected def add : (α →ₘ γ) → (α →ₘ γ) → (α →ₘ γ) :=
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ └┘
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ └┘
269 comp₂ (+) (measurable.add (measurable.fst measurable_id) (measurable.snd measurable_id))
id └───┘ ┴ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
src └───┘ ┴ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └───┘ ┴ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
doc └───┘
270
271 instance : has_add (α →ₘ γ) := ⟨ae_eq_fun.add⟩
id └─────┘ ┴ └┘ ┴ └───────────┘
src └─────┘ └┘ └───────────┘
typ └─────┘ ┴ └┘ ┴ └───────────┘
doc └┘
272
273 @[simp] lemma mk_add_mk (f g : α → γ) (hf hg) :
id ┴ ┴
typ ┴ ┴
doc └──┘
274 (mk f hf) + (mk g hg) = mk (f + g) (measurable.add hf hg) := rfl
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └────────────┘ └┘ └┘ └─┘
src └┘ ┴ └┘ ┴ └┘ ┴ └────────────┘ └─┘
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └────────────┘ └┘ └┘ └─┘
doc └┘ └┘ └┘
275
276 lemma add_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f + g).to_fun a = f.to_fun a + g.to_fun a :=
id ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘ └─────┘
277 comp₂_to_fun _ _ _ _
id └──────────┘
src └──────────┘
typ └──────────┘
278
279 instance : add_monoid (α →ₘ γ) :=
id └────────┘ ┴ └┘ ┴
src └────────┘ └┘
typ └────────┘ ┴ └┘ ┴
doc └┘
280 { zero := 0,
281 add := ae_eq_fun.add,
id └───────────┘
src └───────────┘
typ └───────────┘
282 add_zero := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_zero _),
id └────────────┘ └────────────┘ └──────┘
src └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└─┘
typ └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└─┘
doc └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
txt └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
par └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
pid └──┘ ┴ ┴ ┴ ┴ └──┘ └─┘
st └────────────────────────────────────────────────────────────────────────┘
283 zero_add := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, zero_add _),
id └────────────┘ └────────────┘ └──────┘
src └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└─┘
typ └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└─┘
doc └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
txt └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
par └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
pid └──┘ ┴ ┴ ┴ ┴ └──┘ └─┘
st └────────────────────────────────────────────────────────────────────────┘
284 add_assoc :=
285 by rintros ⟨a⟩ ⟨b⟩ ⟨c⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_assoc _ _ _) }
id └────────────┘ └────────────┘ └───────┘
src └─────────────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└───────┘└──────┘
typ └─────────────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└───────┘└──────┘
doc └─────────────────┘ └────┘ ┴ ┴ ┴ └──┘ └──────┘
txt └─────────────────┘ └────┘ ┴ ┴ ┴ └──┘ └──────┘
par └─────────────────┘ └────┘ ┴ ┴ ┴ └──┘ └──────┘
pid └──────────┘ ┴ ┴ ┴ ┴ └──┘ └─────┘┴
st └──────────────────────────────────────────────────────────────────────────────────────┘
286
287 end add_monoid
288
289 section add_comm_monoid
290 variables {γ : Type*}
291 [topological_space γ] [second_countable_topology γ] [add_comm_monoid γ] [topological_add_monoid γ]
id └───────────────┘ └───────────────────────┘ └─────────────┘ └────────────────────┘
src └───────────────┘ └───────────────────────┘ └─────────────┘ └────────────────────┘
typ └───────────────┘ └───────────────────────┘ └─────────────┘ └────────────────────┘
doc └───────────────┘ └───────────────────────┘ └────────────────────┘
292
293 instance add_comm_monoid : add_comm_monoid (α →ₘ γ) :=
id └─────────────┘ ┴ └┘ ┴
src └─────────────┘ └┘
typ └─────────────┘ ┴ └┘ ┴
doc └┘
294 { add_comm := by rintros ⟨a⟩ ⟨b⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_comm _ _),
id └────────────┘ └────────────┘ └──────┘
src └─────────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└───┘
typ └─────────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────┘└───┘
doc └─────────────┘ └────┘ ┴ ┴ ┴ └──┘ └───┘
txt └─────────────┘ └────┘ ┴ ┴ ┴ └──┘ └───┘
par └─────────────┘ └────┘ ┴ ┴ ┴ └──┘ └───┘
pid └──────┘ ┴ ┴ ┴ ┴ └──┘ └───┘
st └──────────────────────────────────────────────────────────────────────────────┘
295 .. ae_eq_fun.add_monoid }
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
296
297 end add_comm_monoid
298
299 section add_group
300
301 variables {γ : Type*} [topological_space γ] [add_group γ] [topological_add_group γ]
id └───────────────┘ └───────┘ └───────────────────┘
src └───────────────┘ └───────┘ └───────────────────┘
typ └───────────────┘ └───────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
302
303 protected def neg : (α →ₘ γ) → (α →ₘ γ) := comp has_neg.neg (measurable.neg measurable_id)
id ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └─────────┘ └────────────┘ └───────────┘
src └┘ └┘ └──┘ └─────────┘ └────────────┘ └───────────┘
typ ┴ └┘ ┴ ┴ └┘ ┴ └──┘ └─────────┘ └────────────┘ └───────────┘
doc └┘ └┘ └──┘
304
305 instance : has_neg (α →ₘ γ) := ⟨ae_eq_fun.neg⟩
id └─────┘ ┴ └┘ ┴ └───────────┘
src └─────┘ └┘ └───────────┘
typ └─────┘ ┴ └┘ ┴ └───────────┘
doc └┘
306
307 @[simp] lemma neg_mk (f : α → γ) (hf) : -(mk f hf) = mk (-f) (measurable.neg hf) := rfl
id ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └────────────┘ └┘ └─┘
src ┴ └┘ ┴ └┘ ┴ └────────────┘ └─┘
typ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └────────────┘ └┘ └─┘
doc └──┘ └┘ └┘
308
309 lemma neg_to_fun (f : α →ₘ γ) : ∀ₘ a, (-f).to_fun a = - f.to_fun a := comp_to_fun _ _ _
id ┴ └┘ ┴ └┘ ┴┴ ┴┴ └────┘ ┴ ┴ ┴ ┴└─────┘ ┴ └─────────┘
src └┘ └┘ ┴ ┴ └────┘ ┴ ┴ └─────┘ └─────────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴┴ └────┘ ┴ ┴ ┴ ┴└─────┘ ┴ └─────────┘
doc └┘ └┘ ┴ └────┘ └─────┘
310
311 variables [second_countable_topology γ]
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
doc └───────────────────────┘
312 instance : add_group (α →ₘ γ) :=
id └───────┘ ┴ └┘ ┴
src └───────┘ └┘
typ └───────┘ ┴ └┘ ┴
doc └┘
313 { neg := ae_eq_fun.neg,
id └───────────┘
src └───────────┘
typ └───────────┘
314 add_left_neg := by rintros ⟨a⟩; exact quotient.sound (univ_mem_sets' $ assume a, add_left_neg _),
id └────────────┘ └────────────┘ └──────────┘
src └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────────┘└─┘
typ └─────────┘ └────┘└────────────┘┴ └────────────┘┴ ┴ └──┘└──────────┘└─┘
doc └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
txt └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
par └─────────┘ └────┘ ┴ ┴ ┴ └──┘ └─┘
pid └──┘ ┴ ┴ ┴ ┴ └──┘ └─┘
st └────────────────────────────────────────────────────────────────────────────┘
315 .. ae_eq_fun.add_monoid
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
316 }
317
318 @[simp] lemma mk_sub_mk (f g : α → γ) (hf hg) :
id ┴ ┴
typ ┴ ┴
doc └──┘
319 (mk f hf) - (mk g hg) = mk (λa, (f a) - (g a)) (measurable.sub hf hg) := rfl
id └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘ └─┘
src └┘ ┴ └┘ ┴ └┘ ┴ └────────────┘ └─┘
typ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ └┘ └┘ └─┘
doc └┘ └┘ └┘
320
321 lemma sub_to_fun (f g : α →ₘ γ) : ∀ₘ a, (f - g).to_fun a = f.to_fun a - g.to_fun a :=
id ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ └─────┘ ┴ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴└─────┘ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘ └─────┘
322 begin
st └─────
323 rw sub_eq_add_neg,
id └────────────┘
src └─┘└────────────┘
typ └─┘└────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────┘└─
324 filter_upwards [add_to_fun f (-g), neg_to_fun g],
id └────────┘ ┴ ┴┴ └────────┘ ┴
src └──────────────┘└────────┘┴ ┴ ┴ └─┘└────────┘┴ ┴
typ └──────────────┘└────────┘┴┴┴ ┴┴└─┘└────────┘┴┴┴
doc └──────────────┘ ┴ ┴ └─┘ ┴ ┴
txt └──────────────┘ ┴ ┴ └─┘ ┴ ┴
par └──────────────┘ ┴ ┴ └─┘ ┴ ┴
pid └┘ ┴ ┴ └─┘ ┴ ┴
st ─────────────────────────────────────────────────┘└─
325 assume a,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
326 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
327 repeat {assume h, rw h},
id ┴
src └──────┘└──────┘└┘└─┘ ┴
typ └──────┘└──────┘└┘└─┘┴┴
doc └──────┘└──────┘└┘└─┘ ┴
txt └──────┘└──────┘└┘└─┘ ┴
par └──────┘└──────┘└┘└─┘ ┴
pid └─────────────┘ ┴
st ─────────────────┘└────┘└┘└
328 refl
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────┘
329 end
st └─┘
330
331 end add_group
332
333 section add_comm_group
334
335 variables {γ : Type*}
336 [topological_space γ] [second_countable_topology γ] [add_comm_group γ] [topological_add_group γ]
id └───────────────┘ └───────────────────────┘ └────────────┘ └───────────────────┘
src └───────────────┘ └───────────────────────┘ └────────────┘ └───────────────────┘
typ └───────────────┘ └───────────────────────┘ └────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────────┘ └───────────────────┘
337
338 instance : add_comm_group (α →ₘ γ) :=
id └────────────┘ ┴ └┘ ┴
src └────────────┘ └┘
typ └────────────┘ ┴ └┘ ┴
doc └┘
339 { add_comm := ae_eq_fun.add_comm_monoid.add_comm
id └───────────────────────┘└───────┘
src └───────────────────────┘└───────┘
typ └───────────────────────┘└───────┘
340 .. ae_eq_fun.add_group
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
341 }
342
343 end add_comm_group
344
345 section semimodule
346
347 variables {𝕜 : Type*} [semiring 𝕜] [topological_space 𝕜]
id └──────┘ └───────────────┘
src └──────┘ └───────────────┘
typ └──────┘ └───────────────┘
doc └───────────────┘
348 variables {γ : Type*} [topological_space γ]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
349 [add_comm_monoid γ] [semimodule 𝕜 γ] [topological_semimodule 𝕜 γ]
id └─────────────┘ └────────┘ └────────────────────┘
src └─────────────┘ └────────┘ └────────────────────┘
typ └─────────────┘ └────────┘ └────────────────────┘
doc └────────┘ └────────────────────┘
350
351 protected def smul : 𝕜 → (α →ₘ γ) → (α →ₘ γ) :=
id ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘
typ ┴ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
352 λ c f, comp (has_scalar.smul c) (measurable.smul _ measurable_id) f
id ┴ ┴ └──┘ └─────────────┘ ┴ └─────────────┘ └───────────┘ ┴
src └──┘ └─────────────┘ └─────────────┘ └───────────┘
typ ┴ ┴ └──┘ └─────────────┘ ┴ └─────────────┘ └───────────┘ ┴
doc └──┘
353
354 instance : has_scalar 𝕜 (α →ₘ γ) := ⟨ae_eq_fun.smul⟩
id └────────┘ ┴ ┴ └┘ ┴ └────────────┘
src └────────┘ └┘ └────────────┘
typ └────────┘ ┴ ┴ └┘ ┴ └────────────┘
doc └────────┘ └┘
355
356 @[simp] lemma smul_mk (c : 𝕜) (f : α → γ) (hf) : c • (mk f hf) = mk (c • f) (measurable.smul _ hf) :=
id ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────────────┘ └┘
src ┴ └┘ ┴ └┘ ┴ └─────────────┘
typ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └─────────────┘ └┘
doc └──┘ └┘ └┘
357 rfl
id └─┘
src └─┘
typ └─┘
358
359 lemma smul_to_fun (c : 𝕜) (f : α →ₘ γ) : ∀ₘ a, (c • f).to_fun a = c • f.to_fun a :=
id ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
src └┘ └┘ ┴ ┴ └────┘ ┴ ┴ └─────┘
typ ┴ ┴ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘
360 comp_to_fun _ _ _
id └─────────┘
src └─────────┘
typ └─────────┘
361
362 variables [second_countable_topology γ] [topological_add_monoid γ]
id └───────────────────────┘ └────────────────────┘
src └───────────────────────┘ └────────────────────┘
typ └───────────────────────┘ └────────────────────┘
doc └───────────────────────┘ └────────────────────┘
363
364 instance : semimodule 𝕜 (α →ₘ γ) :=
id └────────┘ ┴ ┴ └┘ ┴
src └────────┘ └┘
typ └────────┘ ┴ ┴ └┘ ┴
doc └────────┘ └┘
365 { one_smul := by { rintros ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, one_smul] },
id └───────────┘ └─────┘ └──────┘
src └─────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└──────┘└┘
typ └─────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└──────┘└┘
doc └─────────────┘ └─────────┘ └┘ └┘ └┘
txt └─────────────┘ └─────────┘ └┘ └┘ └┘
par └─────────────┘ └─────────┘ └┘ └┘ └┘
pid └──────┘ ┴└──┘└┘ └┘ └┘ ┴┴
st └────────────────┘└─────────────────────────────────────────────┘└┘
366 mul_smul :=
367 by { rintros x y ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, mul_action.mul_smul x y f], refl },
id └───────────┘ └─────┘ └─────────────────┘ ┴ ┴ ┴
src └─────────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└─────────────────┘┴ ┴ ┴ ┴ └───┘
typ └─────────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└─────────────────┘┴┴┴┴┴┴┴ └───┘
doc └─────────────────┘ └─────────┘ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
txt └─────────────────┘ └─────────┘ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
par └─────────────────┘ └─────────┘ └┘ └┘ ┴ ┴ ┴ ┴ └───┘
pid └──────────┘ ┴└──┘└┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
st └────────────────────┘└─────────────────────────────────────────────────────────────┘└─────┘└┘
368 smul_add :=
369 begin
st └─────
370 rintros x ⟨f, hf⟩ ⟨g, hg⟩, simp only [quot_mk_eq_mk, smul_mk, mk_add_mk],
id └───────────┘ └─────┘ └───────┘
src └───────────────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└───────┘┴
typ └───────────────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└───────┘┴
doc └───────────────────────┘ └─────────┘ └┘ └┘ ┴
txt └───────────────────────┘ └─────────┘ └┘ └┘ ┴
par └───────────────────────┘ └─────────┘ └┘ └┘ ┴
pid └────────────────┘ ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────┘└─────────────────────────────────────────────┘└─
371 congr, exact smul_add x f g
id └──────┘ ┴ ┴ ┴
src └───┘ └────┘└──────┘┴ ┴ ┴ └
typ └───┘ └────┘└──────┘┴┴┴┴┴┴└
doc └────┘ ┴ ┴ ┴ └
txt └───┘ └────┘ ┴ ┴ ┴ └
par └───┘ └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st ────────┘└──────────────────────
372 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
373 smul_zero := by { intro x, simp only [zero_def, smul_mk], congr, exact smul_zero x },
id └──────┘ └─────┘ └───────┘ ┴
src └─────┘ └─────────┘└──────┘└┘└─────┘┴ └───┘ └────┘└───────┘┴ ┴
typ └─────┘ └─────────┘└──────┘└┘└─────┘┴ └───┘ └────┘└───────┘┴┴┴
doc └─────┘ └─────────┘ └┘ ┴ └────┘ ┴ ┴
txt └─────┘ └─────────┘ └┘ ┴ └───┘ └────┘ ┴ ┴
par └─────┘ └─────────┘ └┘ ┴ └───┘ └────┘ ┴ ┴
pid └┘ ┴└──┘└┘ └┘ ┴ ┴ ┴ ┴
st └────────┘└─────────────────────────────┘└─────┘└──────────────────┘└┘
374 add_smul :=
375 begin
st └─────
376 intros x y, rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, mk_add_mk], congr,
id └───────────┘ └─────┘ └───────┘
src └────────┘ └────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└───────┘┴ └───┘
typ └────────┘ └────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└───────┘┴ └───┘
doc └────────┘ └────────────┘ └─────────┘ └┘ └┘ ┴
txt └────────┘ └────────────┘ └─────────┘ └┘ └┘ ┴ └───┘
par └────────┘ └────────────┘ └─────────┘ └┘ └┘ ┴ └───┘
pid └──┘ └──────┘ ┴└──┘└┘ └┘ └┘ ┴
st ─────────────┘└──────────────┘└─────────────────────────────────────────────┘└─────┘└─
377 exact add_smul x y f
id └──────┘ ┴ ┴ ┴
src └────┘└──────┘┴ ┴ ┴ └
typ └────┘└──────┘┴┴┴┴┴┴└
doc └────┘ ┴ ┴ ┴ └
txt └────┘ ┴ ┴ ┴ └
par └────┘ ┴ ┴ ┴ └
pid ┴ ┴ ┴ ┴ └
st ─────────────────────────
378 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
379 zero_smul :=
380 by { rintro ⟨f, hf⟩, simp only [quot_mk_eq_mk, smul_mk, zero_def], congr, exact zero_smul 𝕜 f }}
id └───────────┘ └─────┘ └──────┘ └───────┘ ┴ ┴
src └────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└──────┘┴ └───┘ └────┘└───────┘┴ ┴ ┴
typ └────────────┘ └─────────┘└───────────┘└┘└─────┘└┘└──────┘┴ └───┘ └────┘└───────┘┴┴┴┴┴
doc └────────────┘ └─────────┘ └┘ └┘ ┴ └────┘ ┴ ┴ ┴
txt └────────────┘ └─────────┘ └┘ └┘ ┴ └───┘ └────┘ ┴ ┴ ┴
par └────────────┘ └─────────┘ └┘ └┘ ┴ └───┘ └────┘ ┴ ┴ ┴
pid └──────┘ ┴└──┘└┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴
st └───────────────┘└────────────────────────────────────────────┘└─────┘└────────────────────┘└┘
381
382 instance : mul_action 𝕜 (α →ₘ γ) := by apply_instance
id └────────┘ ┴ ┴ └┘ ┴
src └────────┘ └┘ └──────────────
typ └────────┘ ┴ ┴ └┘ ┴ └──────────────
doc └────────┘ └┘ └──────────────
txt └──────────────
par └──────────────
pid └
st └───────────────
383
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
384 end semimodule
385
386 section module
387
388 variables {𝕜 : Type*} [ring 𝕜] [topological_space 𝕜]
id └──┘ └───────────────┘
src └──┘ └───────────────┘
typ └──┘ └───────────────┘
doc └───────────────┘
389 variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
id └───────────────┘ └───────────────────────┘ └────────────┘
src └───────────────┘ └───────────────────────┘ └────────────┘
typ └───────────────┘ └───────────────────────┘ └────────────┘
doc └───────────────┘ └───────────────────────┘
390 [topological_add_group γ] [module 𝕜 γ] [topological_semimodule 𝕜 γ]
id └───────────────────┘ └────┘ └────────────────────┘
src └───────────────────┘ └────┘ └────────────────────┘
typ └───────────────────┘ └────┘ └────────────────────┘
doc └───────────────────┘ └────┘ └────────────────────┘
391
392 instance : module 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }
id └────┘ ┴ ┴ └┘ ┴ └──────────────────┘
src └────┘ └┘ └──────────────────┘
typ └────┘ ┴ ┴ └┘ ┴ └──────────────────┘
doc └────┘ └┘
393
394 end module
395
396 section vector_space
397
398 variables {𝕜 : Type*} [discrete_field 𝕜] [topological_space 𝕜]
id └────────────┘ └───────────────┘
src └────────────┘ └───────────────┘
typ └────────────┘ └───────────────┘
doc └───────────────┘
399 variables {γ : Type*} [topological_space γ] [second_countable_topology γ] [add_comm_group γ]
id └───────────────┘ └───────────────────────┘ └────────────┘
src └───────────────┘ └───────────────────────┘ └────────────┘
typ └───────────────┘ └───────────────────────┘ └────────────┘
doc └───────────────┘ └───────────────────────┘
400 [topological_add_group γ] [vector_space 𝕜 γ] [topological_semimodule 𝕜 γ]
id └───────────────────┘ └──────────┘ └────────────────────┘
src └───────────────────┘ └──────────┘ └────────────────────┘
typ └───────────────────┘ └──────────┘ └────────────────────┘
doc └───────────────────┘ └──────────┘ └────────────────────┘
401
402 instance : vector_space 𝕜 (α →ₘ γ) := { .. ae_eq_fun.semimodule }
id └──────────┘ ┴ ┴ └┘ ┴ └──────────────────┘
src └──────────┘ └┘ └──────────────────┘
typ └──────────┘ ┴ ┴ └┘ ┴ └──────────────────┘
doc └──────────┘ └┘
403
404 end vector_space
405
406 /- TODO : Prove that `L⁰` is a complete space if the codomain is complete. -/
407 /- TODO : Multiplicative structure of `L⁰` if useful -/
408
409 open ennreal
410
411 /-- For `f : α → ennreal`, Define `∫ [f]` to be `∫ f` -/
412 def eintegral (f : α →ₘ ennreal) : ennreal :=
id ┴ └┘ └─────┘ └─────┘
src └┘ └─────┘ └─────┘
typ ┴ └┘ └─────┘ └─────┘
doc └┘ └─────┘ └─────┘
413 quotient.lift_on f (λf, lintegral f.1) (assume ⟨f, hf⟩ ⟨g, hg⟩ eq, lintegral_congr_ae eq)
id └──────────────┘ ┴ ┴ └───────┘ ┴┴ ┴ ┴ └┘ └────────────────┘ └┘
src └──────────────┘ └───────┘ ┴ └┘ └────────────────┘ └┘
typ └──────────────┘ ┴ ┴ └───────┘ ┴┴ ┴ ┴ └┘ └────────────────┘ └┘
doc └───────┘
414
415 @[simp] lemma eintegral_mk (f : α → ennreal) (hf) : eintegral (mk f hf) = lintegral f := rfl
id ┴ └─────┘ └───────┘ └┘ ┴ └┘ ┴ └───────┘ ┴ └─┘
src └─────┘ └───────┘ └┘ ┴ └───────┘ └─┘
typ ┴ └─────┘ └───────┘ └┘ ┴ └┘ ┴ └───────┘ ┴ └─┘
doc └──┘ └─────┘ └───────┘ └┘ └───────┘
416
417 lemma eintegral_to_fun (f : α →ₘ ennreal) : eintegral f = lintegral (f.to_fun) :=
id ┴ └┘ └─────┘ └───────┘ ┴ ┴ └───────┘ ┴└─────┘
src └┘ └─────┘ └───────┘ ┴ └───────┘ └─────┘
typ ┴ └┘ └─────┘ └───────┘ ┴ ┴ └───────┘ ┴└─────┘
doc └┘ └─────┘ └───────┘ └───────┘ └─────┘
418 by conv_lhs { rw [self_eq_mk f, eintegral_mk] }
id └────────┘ ┴ └──────────┘
src └─────────┘└──┘└────────┘┴ └┘└──────────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└──────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└────────────┘ ┴┴└
419
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
420 @[simp] lemma eintegral_zero : eintegral (0 : α →ₘ ennreal) = 0 := lintegral_zero
id └───────┘ ┴ └┘ └─────┘ ┴ └────────────┘
src └───────┘ └┘ └─────┘ ┴ └────────────┘
typ └───────┘ ┴ └┘ └─────┘ ┴ └────────────┘
doc └──┘ └───────┘ └┘ └─────┘
421
422 @[simp] lemma eintegral_eq_zero_iff (f : α →ₘ ennreal) : eintegral f = 0 ↔ f = 0 :=
id ┴ └┘ └─────┘ └───────┘ ┴ ┴ ┴ ┴ ┴
src └┘ └─────┘ └───────┘ ┴ ┴ ┴
typ ┴ └┘ └─────┘ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘ └┘ └─────┘ └───────┘
423 begin
st └─────
424 rcases f with ⟨f, hf⟩,
id ┴
src └─────┘ └───────────┘
typ └─────┘┴└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ──────────────────────┘└─
425 refine iff.trans (lintegral_eq_zero_iff hf) ⟨_, _⟩,
id └───────┘ └───────────────────┘ └┘
src └─────┘└───────┘┴ └───────────────────┘┴ └┘ └───┘
typ └─────┘└───────┘┴ └───────────────────┘┴└┘└┘ └───┘
doc └─────┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ └┘ └───┘
pid ┴ ┴ ┴ └┘ └───┘
st ───────────────────────────────────────────────────┘└─
426 { assume h, exact quotient.sound h },
id └────────────┘ ┴
src └──────┘ └────┘└────────────┘┴ ┴
typ └──────┘ └────┘└────────────┘┴┴┴
doc └──────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ ┴ ┴
par └──────┘ └────┘ ┴ ┴
pid └──────┘ ┴ ┴ ┴
st ───┘└──────┘└───────────────────────┘└┘└
427 { assume h, exact quotient.exact h }
id └────────────┘ ┴
src └──────┘ └────┘└────────────┘┴ ┴
typ └──────┘ └────┘└────────────┘┴┴┴
doc └──────┘ └────┘ ┴ ┴
txt └──────┘ └────┘ ┴ ┴
par └──────┘ └────┘ ┴ ┴
pid └──────┘ ┴ ┴ ┴
st ───────────┘└───────────────────────┘└─
428 end
st ──┘
429
430 lemma eintegral_add : ∀(f g : α →ₘ ennreal), eintegral (f + g) = eintegral f + eintegral g :=
id ┴ └┘ └─────┘ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └┘ └─────┘ └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ ┴ └┘ └─────┘ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
doc └┘ └─────┘ └───────┘ └───────┘ └───────┘
431 by { rintros ⟨f⟩ ⟨g⟩, simp only [quot_mk_eq_mk, mk_add_mk, eintegral_mk], exact lintegral_add f.2 g.2 }
id └───────────┘ └───────┘ └──────────┘ └───────────┘ ┴ ┴
src └─────────────┘ └─────────┘└───────────┘└┘└───────┘└┘└──────────┘┴ └────┘└───────────┘┴ └─┘ └─┘
typ └─────────────┘ └─────────┘└───────────┘└┘└───────┘└┘└──────────┘┴ └────┘└───────────┘┴┴└─┘┴└─┘
doc └─────────────┘ └─────────┘ └┘ └┘ ┴ └────┘ ┴ └─┘ └─┘
txt └─────────────┘ └─────────┘ └┘ └┘ ┴ └────┘ ┴ └─┘ └─┘
par └─────────────┘ └─────────┘ └┘ └┘ ┴ └────┘ ┴ └─┘ └─┘
pid └──────┘ ┴└──┘└┘ └┘ └┘ ┴ ┴ ┴ └─┘ └─┘
st └────────────────┘└──────────────────────────────────────────────────┘└────────────────────────────┘└┘
432
433 lemma eintegral_le_eintegral {f g : α →ₘ ennreal} (h : f ≤ g) : eintegral f ≤ eintegral g :=
id ┴ └┘ └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └┘ └─────┘ ┴ └───────┘ ┴ └───────┘
typ ┴ └┘ └─────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
doc └┘ └─────┘ └───────┘ └───────┘
434 begin
st └─────
435 rcases f with ⟨f, hf⟩, rcases g with ⟨g, hg⟩,
id ┴ ┴
src └─────┘ └───────────┘ └─────┘ └───────────┘
typ └─────┘┴└───────────┘ └─────┘┴└───────────┘
doc └─────┘ └───────────┘ └─────┘ └───────────┘
txt └─────┘ └───────────┘ └─────┘ └───────────┘
par └─────┘ └───────────┘ └─────┘ └───────────┘
pid ┴ └───────────┘ ┴ └───────────┘
st ──────────────────────┘└─────────────────────┘└─
436 simp only [quot_mk_eq_mk, eintegral_mk, mk_le_mk] at *,
id └───────────┘ └──────────┘ └──────┘
src └─────────┘└───────────┘└┘└──────────┘└┘└──────┘└────┘
typ └─────────┘└───────────┘└┘└──────────┘└┘└──────┘└────┘
doc └─────────┘ └┘ └┘ └────┘
txt └─────────┘ └┘ └┘ └────┘
par └─────────┘ └┘ └┘ └────┘
pid ┴└──┘└┘ └┘ └┘ ┴┴└──┘
st ───────────────────────────────────────────────────────┘└─
437 refine lintegral_le_lintegral_ae _,
id └───────────────────────┘
src └─────┘└───────────────────────┘└┘
typ └─────┘└───────────────────────┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴ └┘
st ───────────────────────────────────┘└─
438 filter_upwards [h], simp
src └──────────────┘ ┴ └───┘
typ └──────────────┘ ┴ └───┘
doc └──────────────┘ ┴ └───┘
txt └──────────────┘ ┴ └───┘
par └──────────────┘ ┴ └───┘
pid └┘ ┴ ┴
st ───────────────────┘└─────┘
439 end
st └─┘
440
441 section
442 variables {γ : Type*} [emetric_space γ] [second_countable_topology γ]
id └───────────┘ └───────────────────────┘
src └───────────┘ └───────────────────────┘
typ └───────────┘ └───────────────────────┘
doc └───────────┘ └───────────────────────┘
443
444 /-- `comp_edist [f] [g] a` will return `edist (f a) (g a) -/
445 def comp_edist (f g : α →ₘ γ) : α →ₘ ennreal := comp₂ edist measurable_edist f g
id ┴ └┘ ┴ ┴ └┘ └─────┘ └───┘ └───┘ └──────────────┘ ┴ ┴
src └┘ └┘ └─────┘ └───┘ └───┘ └──────────────┘
typ ┴ └┘ ┴ ┴ └┘ └─────┘ └───┘ └───┘ └──────────────┘ ┴ ┴
doc └┘ └┘ └─────┘ └───┘
446
447 lemma comp_edist_to_fun (f g : α →ₘ γ) :
id ┴ └┘ ┴
src └┘
typ ┴ └┘ ┴
doc └┘
448 ∀ₘ a, (comp_edist f g).to_fun a = edist (f.to_fun a) (g.to_fun a) :=
id └┘ ┴┴ └────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
src └┘ ┴ └────────┘ └────┘ ┴ └───┘ └─────┘ └─────┘
typ └┘ ┴┴ └────────┘ ┴ ┴ └────┘ ┴ ┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
doc └┘ ┴ └────────┘ └────┘ └─────┘ └─────┘
449 comp₂_to_fun _ _ _ _
id └──────────┘
src └──────────┘
typ └──────────┘
450
451 lemma comp_edist_self : ∀ (f : α →ₘ γ), comp_edist f f = 0 :=
id ┴ └┘ ┴ └────────┘ ┴ ┴ ┴
src └┘ └────────┘ ┴
typ ┴ └┘ ┴ └────────┘ ┴ ┴ ┴
doc └┘ └────────┘
452 by rintro ⟨f⟩; refine quotient.sound _; simp only [edist_self]
id └────────────┘ └────────┘
src └────────┘ └─────┘└────────────┘└┘ └─────────┘└────────┘└─
typ └────────┘ └─────┘└────────────┘└┘ └─────────┘└────────┘└─
doc └────────┘ └─────┘ └┘ └─────────┘ └─
txt └────────┘ └─────┘ └┘ └─────────┘ └─
par └────────┘ └─────┘ └┘ └─────────┘ └─
pid └──┘ ┴ └┘ ┴└──┘└┘ ┴└
st └────────────────────────────────────────────────────────────
453
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
454 /-- Almost everywhere equal functions form an `emetric_space`, with the emetric defined as
455 `edist f g = ∫⁻ a, edist (f a) (g a)`. -/
456 instance : emetric_space (α →ₘ γ) :=
id └───────────┘ ┴ └┘ ┴
src └───────────┘ └┘
typ └───────────┘ ┴ └┘ ┴
doc └───────────┘ └┘
457 { edist := λf g, eintegral (comp_edist f g),
id ┴ ┴ ┴ └───────┘ └────────┘ ┴ ┴
src ┴ └───────┘ └────────┘
typ ┴ ┴ ┴ └───────┘ └────────┘ ┴ ┴
doc └───────┘ └────────┘
458 edist_self := assume f, (eintegral_eq_zero_iff _).2 (comp_edist_self _),
id ┴ └───────────────────┘ ┴ └─────────────┘
src └───────────────────┘ ┴ └─────────────┘
typ ┴ └───────────────────┘ ┴ └─────────────┘
459 edist_comm :=
460 by rintros ⟨f⟩ ⟨g⟩; simp only [comp_edist, quot_mk_eq_mk, comp₂_mk_mk, edist_comm],
id └────────┘ └───────────┘ └─────────┘ └────────┘
src └─────────────┘ └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘└────────┘┴
typ └─────────────┘ └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘└────────┘┴
doc └─────────────┘ └─────────┘└────────┘└┘ └┘ └┘ ┴
txt └─────────────┘ └─────────┘ └┘ └┘ └┘ ┴
par └─────────────┘ └─────────┘ └┘ └┘ └┘ ┴
pid └──────┘ ┴└──┘└┘ └┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────────────────────┘
461 edist_triangle :=
462 begin
st └─────
463 rintros ⟨f⟩ ⟨g⟩ ⟨h⟩,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └──────────┘
st ──────────────────────┘└─
464 simp only [comp_edist, quot_mk_eq_mk, comp₂_mk_mk, (eintegral_add _ _).symm],
id └────────┘ └───────────┘ └─────────┘ └───────────┘
src └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘ └───────────┘└─────────┘
typ └─────────┘└────────┘└┘└───────────┘└┘└─────────┘└┘ └───────────┘└─────────┘
doc └─────────┘└────────┘└┘ └┘ └┘ └─────────┘
txt └─────────┘ └┘ └┘ └┘ └─────────┘
par └─────────┘ └┘ └┘ └┘ └─────────┘
pid ┴└──┘└┘ └┘ └┘ └┘ └─────────┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
465 exact lintegral_le_lintegral _ _ (assume a, edist_triangle _ _ _)
id └────────────────────┘ └────────────┘
src └────┘└────────────────────┘└───┘ └──┘└────────────┘└───────
typ └────┘└────────────────────┘└───┘ └──┘└────────────┘└───────
doc └────┘ └───┘ └──┘ └───────
txt └────┘ └───┘ └──┘ └───────
par └────┘ └───┘ └──┘ └───────
pid ┴ └───┘ └──┘ └─────┘└
st ──────────────────────────────────────────────────────────────────────
466 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
467 eq_of_edist_eq_zero :=
468 begin
st └─────
469 rintros ⟨f⟩ ⟨g⟩,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └──────┘
st ──────────────────┘└─
470 simp only [edist, comp_edist, quot_mk_eq_mk, comp₂_mk_mk, eintegral_eq_zero_iff],
id └────────┘ └───────────┘ └─────────┘ └───────────────────┘
src └─────────┘ └┘└────────┘└┘└───────────┘└┘└─────────┘└┘└───────────────────┘┴
typ └─────────┘ └┘└────────┘└┘└───────────┘└┘└─────────┘└┘└───────────────────┘┴
doc └─────────┘ └┘└────────┘└┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
471 simp only [zero_def, mk_eq_mk, edist_eq_zero],
id └──────┘ └──────┘ └───────────┘
src └─────────┘└──────┘└┘└──────┘└┘└───────────┘┴
typ └─────────┘└──────┘└┘└──────┘└┘└───────────┘┴
doc └─────────┘ └┘ └┘└───────────┘┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ────────────────────────────────────────────────┘└─
472 assume h, assumption
src └──────┘ └──────────
typ └──────┘ └──────────
doc └──────┘ └──────────
txt └──────┘ └──────────
par └──────┘ └──────────
pid └──────┘ └
st ───────────┘└────────────
473 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
474
475 lemma edist_mk_mk {f g : α → γ} (hf hg) : edist (mk f hf) (mk g hg) = ∫⁻ x, edist (f x) (g x) := rfl
id ┴ ┴ └───┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─┘
src └───┘ └┘ └┘ ┴ └┘ ┴ └───┘ └─┘
typ ┴ ┴ └───┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ └─┘
doc └┘ └┘ └┘ ┴
476
477 lemma edist_to_fun (f g : α →ₘ γ) : edist f g = ∫⁻ x, edist (f.to_fun x) (g.to_fun x) :=
id ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
src └┘ └───┘ ┴ └┘ ┴ └───┘ └─────┘ └─────┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └─────┘ └─────┘
478 by conv_lhs { rw [self_eq_mk f, self_eq_mk g, edist_mk_mk] }
id └────────┘ ┴ └────────┘ ┴ └─────────┘
src └─────────┘└──┘└────────┘┴ └┘└────────┘┴ └┘└─────────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└────────┘┴┴└┘└─────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└────────────┘└───────────┘ ┴┴└
479
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
480 lemma edist_zero_to_fun [has_zero γ] (f : α →ₘ γ) : edist f 0 = ∫⁻ x, edist (f.to_fun x) 0 :=
id └──────┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴
src └──────┘ └┘ └───┘ ┴ └┘ ┴ └───┘ └─────┘
typ └──────┘ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └┘ ┴┴ └───┘ ┴└─────┘ ┴
doc └┘ └┘ ┴ └─────┘
481 begin
st └─────
482 rw edist_to_fun,
id └──────────┘
src └─┘└──────────┘
typ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────────────┘└─
483 apply lintegral_congr_ae,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
484 have : ∀ₘ a:α, (0 : α →ₘ γ).to_fun a = 0 := zero_to_fun,
id └┘ ┴ ┴ └┘ ┴ ┴ └─────────┘
src └─────┘└┘└─┘ ┴┴ └──┘ ┴└┘┴ └───────┘ ┴┴└────┘└─────────┘
typ └─────┘└┘└─┘ ┴┴ └──┘┴┴└┘┴┴└───────┘ ┴┴└────┘└─────────┘
doc └─────┘└┘└─┘ ┴┴ └──┘ ┴└┘┴ └───────┘ ┴ └────┘
txt └─────┘ └─┘ ┴ └──┘ ┴ ┴ └───────┘ ┴ └────┘
par └─────┘ └─┘ ┴ └──┘ ┴ ┴ └───────┘ ┴ └────┘
pid └───┘└┘ └─┘ ┴ └──┘ ┴ ┴ └───────┘ ┴ ┴└───┘
st ────────────────────────────────────────────────────────┘└─
485 filter_upwards [this],
src └──────────────┘ ┴
typ └──────────────┘ ┴
doc └──────────────┘ ┴
txt └──────────────┘ ┴
par └──────────────┘ ┴
pid └┘ ┴
st ──────────────────────┘└─
486 assume a h,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───────────┘└─
487 simp only [mem_set_of_eq] at *,
id └───────────┘
src └─────────┘└───────────┘└────┘
typ └─────────┘└───────────┘└────┘
doc └─────────┘ └────┘
txt └─────────┘ └────┘
par └─────────┘ └────┘
pid ┴└──┘└┘ ┴┴└──┘
st ───────────────────────────────┘└─
488 rw h
id ┴
src └─┘ ┴
typ └─┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ──────┘
489 end
st └─┘
490
491 end
492
493 section metric
494 variables {γ : Type*} [metric_space γ] [second_countable_topology γ]
id └──────────┘ └───────────────────────┘
src └──────────┘ └───────────────────────┘
typ └──────────┘ └───────────────────────┘
doc └──────────┘ └───────────────────────┘
495
496 lemma edist_mk_mk' {f g : α → γ} (hf hg) :
id ┴ ┴
typ ┴ ┴
497 edist (mk f hf) (mk g hg) = ∫⁻ x, nndist (f x) (g x) :=
id └───┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
src └───┘ └┘ └┘ ┴ └┘ ┴ └────┘
typ └───┘ └┘ ┴ └┘ └┘ ┴ └┘ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
doc └┘ └┘ └┘ ┴ └────┘
498 show (∫⁻ x, edist (f x) (g x)) = ∫⁻ x, nndist (f x) (g x), from
id └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
src └┘ ┴ └───┘ ┴ └┘ ┴ └────┘
typ └┘ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴ ┴ ┴ ┴
doc └┘ ┴ └┘ ┴ └────┘
499 lintegral_congr_ae $all_ae_of_all $ assume a, edist_nndist _ _
id └────────────────┘ └───────────┘ ┴ └──────────┘
src └────────────────┘ └───────────┘ └──────────┘
typ └────────────────┘ └───────────┘ ┴ └──────────┘
doc └──────────┘
500
501 lemma edist_to_fun' (f g : α →ₘ γ) : edist f g = ∫⁻ x, nndist (f.to_fun x) (g.to_fun x) :=
id ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴└─────┘ ┴ ┴└─────┘ ┴
src └┘ └───┘ ┴ └┘ ┴ └────┘ └─────┘ └─────┘
typ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └┘ ┴┴ └────┘ ┴└─────┘ ┴ ┴└─────┘ ┴
doc └┘ └┘ ┴ └────┘ └─────┘ └─────┘
502 by conv_lhs { rw [self_eq_mk f, self_eq_mk g, edist_mk_mk'] }
id └────────┘ ┴ └────────┘ ┴ └──────────┘
src └─────────┘└──┘└────────┘┴ └┘└────────┘┴ └┘└──────────┘└┘└─
typ └─────────┘└──┘└────────┘┴┴└┘└────────┘┴┴└┘└──────────┘└┘└─
txt └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
par └─────────┘└──┘ ┴ └┘ ┴ └┘ └┘└─
pid ┴└────┘ ┴ └┘ ┴ └┘ └─┘└
st └─────────┘└───────────────┘└────────────┘└────────────┘ ┴┴└
503
src ┘
typ ┘
txt ┘
par ┘
pid ┘
st ┘
504 end metric
505
506 section normed_group
507
508 variables {γ : Type*} [normed_group γ] [second_countable_topology γ]
id └──────────┘ └───────────────────────┘
src └──────────┘ └───────────────────────┘
typ └──────────┘ └───────────────────────┘
doc └──────────┘ └───────────────────────┘
509
510 lemma edist_eq_add_add : ∀ {f g h : α →ₘ γ}, edist f g = edist (f + h) (g + h) :=
id ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └───┘ ┴ └───┘ ┴ ┴
typ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘
511 begin
st └─────
512 rintros ⟨f⟩ ⟨g⟩ ⟨h⟩,
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └──────────┘
st ────────────────────┘└─
513 simp only [quot_mk_eq_mk, mk_add_mk, edist_mk_mk'],
id └───────────┘ └───────┘ └──────────┘
src └─────────┘└───────────┘└┘└───────┘└┘└──────────┘┴
typ └─────────┘└───────────┘└┘└───────┘└┘└──────────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────┘└─
514 apply lintegral_congr_ae,
id └────────────────┘
src └────┘└────────────────┘
typ └────┘└────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────┘└─
515 filter_upwards [], simp [nndist_eq_nnnorm]
id └──────────────┘
src └───────────────┘ └────┘└──────────────┘└┘
typ └───────────────┘ └────┘└──────────────┘└┘
doc └───────────────┘ └────┘ └┘
txt └───────────────┘ └────┘ └┘
par └───────────────┘ └────┘ └┘
pid └─┘ ┴┴ ┴┴
st ──────────────────┘└────────────────────────┘
516 end
st └─┘
517
518 end normed_group
519
520 section normed_space
521
522 set_option class.instance_max_depth 100
doc └──────────────────────┘
523
524 variables {𝕜 : Type*} [normed_field 𝕜]
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
525 variables {γ : Type*} [normed_group γ] [second_countable_topology γ] [normed_space 𝕜 γ]
id └──────────┘ └───────────────────────┘ └──────────┘
src └──────────┘ └───────────────────────┘ └──────────┘
typ └──────────┘ └───────────────────────┘ └──────────┘
doc └──────────┘ └───────────────────────┘ └──────────┘
526
527 lemma edist_smul (x : 𝕜) : ∀ f : α →ₘ γ, edist (x • f) 0 = (ennreal.of_real ∥x∥) * edist f 0 :=
id ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴┴┴ ┴ └───┘ ┴
src └┘ └───┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └───┘
typ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴┴┴ ┴ └───┘ ┴
doc └┘ └─────────────┘
528 begin
st └─────
529 rintros ⟨f, hf⟩, simp only [zero_def, edist_mk_mk', quot_mk_eq_mk, smul_mk],
id └──────┘ └──────────┘ └───────────┘ └─────┘
src └─────────────┘ └─────────┘└──────┘└┘└──────────┘└┘└───────────┘└┘└─────┘┴
typ └─────────────┘ └─────────┘└──────┘└┘└──────────┘└┘└───────────┘└┘└─────┘┴
doc └─────────────┘ └─────────┘ └┘ └┘ └┘ ┴
txt └─────────────┘ └─────────┘ └┘ └┘ └┘ ┴
par └─────────────┘ └─────────┘ └┘ └┘ └┘ ┴
pid └──────┘ ┴└──┘└┘ └┘ └┘ └┘ ┴
st ────────────────┘└──────────────────────────────────────────────────────────┘└─
530 exact calc
src └────┘ └
typ └────┘ └
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ─────────────
531 (∫⁻ (a : α), nndist (x • f a) 0) = (∫⁻ (a : α), (nnnorm x) * nnnorm (f a)) :
id └┘ ┴ └────┘ ┴ ┴ ┴ ┴ └────┘ ┴
src ───┘ └┘└────┘ ┴┴┴└────┘┴ ┴┴┴ ┴ └───┘ ┴ └────┘ ┴ ┴ ┴ └┘┴┴└────┘┴ ┴ └────
typ ───┘ └┘└────┘ ┴┴┴└────┘┴ ┴┴┴ ┴ └───┘ ┴ └────┘┴┴ ┴ ┴┴└┘┴┴└────┘┴ ┴┴ └────
doc ───┘ └┘└────┘ ┴┴┴└────┘┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴└────┘┴ ┴ └────
txt ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────
par ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────
pid ───┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └────
st ─────────────────────────────────────────────────────────────────────────────────
532 lintegral_congr_ae $ by { filter_upwards [], assume a, simp [nndist_eq_nnnorm, nnnorm_smul] }
id └────────────────┘ └──────────────┘ └─────────┘
src ─────┘└────────────────┘┴ ┴ └─┘└───────────────┘└┘└──────┘└┘└────┘└──────────────┘└┘└─────────┘└┘└─
typ ─────┘└────────────────┘┴ ┴ └─┘└───────────────┘└┘└──────┘└┘└────┘└──────────────┘└┘└─────────┘└┘└─
doc ─────┘ ┴ ┴ └─┘└───────────────┘└┘└──────┘└┘└────┘ └┘ └┘└─
txt ─────┘ ┴ ┴ └─┘└───────────────┘└┘└──────┘└┘└────┘ └┘ └┘└─
par ─────┘ ┴ ┴ └─┘└───────────────┘└┘└──────┘└┘└────┘ └┘ └┘└─
pid ─────┘ ┴ ┴ └────────────────────────────────────┘ └┘ └───
st ────────────────────────────┘└──────────────────┘└────────┘└─────────────────────────────────────┘┴└
533 ... = _ : lintegral_const_mul _ (measurable.coe_nnnorm hf)
id └─────────────────┘ └───────────────────┘ └┘
src ───────┘ └───┘└─────────────────┘└─┘ └───────────────────┘┴ └─
typ ───────┘ └───┘└─────────────────┘└─┘ └───────────────────┘┴└┘└─
doc ───────┘ └───┘ └─┘ ┴ └─
txt ───────┘ └───┘ └─┘ ┴ └─
par ───────┘ └───┘ └─┘ ┴ └─
pid ───────┘ └───┘ └─┘ ┴ └─
st ───────────────────────────────────────────────────────────────
534 ... = _ :
src ───────┘ └────
typ ───────┘ └────
doc ───────┘ └────
txt ───────┘ └────
par ───────┘ └────
pid ───────┘ └────
st ──────────────
535 begin
src ───┘ └
typ ───┘ └
doc ───┘ └
txt ───┘ └
par ───┘ └
pid ───┘ └
st ───┘└─────
536 convert rfl,
id └─┘
src ─────┘└──────┘└─┘└─
typ ─────┘└──────┘└─┘└─
doc ─────┘└──────┘ └─
txt ─────┘└──────┘ └─
par ─────┘└──────┘ └─
pid ─────────────┘ └─
st ────────────────┘└─
537 { rw ← coe_nnnorm, rw [ennreal.of_real], congr, exact nnreal.of_real_coe },
id └────────┘ └─────────────┘ └────────────────┘
src ───────┘└───┘└────────┘└┘└──┘└─────────────┘┴└┘└───┘└──────┘└────────────────┘└───
typ ───────┘└───┘└────────┘└┘└──┘└─────────────┘┴└┘└───┘└──────┘└────────────────┘└───
doc ───────┘└───┘ └┘└──┘└─────────────┘┴└┘ └──────┘ └───
txt ───────┘└───┘ └┘└──┘ ┴└┘└───┘└──────┘ └───
par ───────┘└───┘ └┘└──┘ ┴└┘└───┘└──────┘ └───
pid ────────────┘ └────┘ └──────────────┘ └───
st ──────┘└──────────────┘└───────────────────┘└──────┘└─────────────────────────┘┴└─
538 { funext, simp [nndist_eq_nnnorm] }
id └──────────────┘
src ───────┘└────┘└┘└────┘└──────────────┘└┘└─
typ ───────┘└────┘└┘└────┘└──────────────┘└┘└─
doc ───────┘└────┘└┘└────┘ └┘└─
txt ───────┘└────┘└┘└────┘ └┘└─
par ───────┘└────┘└┘└────┘ └┘└─
pid ─────────────────────┘ └───
st ─────────────┘└────────────────────────┘└─
539 end,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ─────────
540 end
st ──┘
541
542 end normed_space
543
544 section pos_part
545
546 variables {γ : Type*} [topological_space γ] [decidable_linear_order γ] [order_closed_topology γ]
id └───────────────┘ └────────────────────┘ └───────────────────┘
src └───────────────┘ └────────────────────┘ └───────────────────┘
typ └───────────────┘ └────────────────────┘ └───────────────────┘
doc └───────────────┘ └───────────────────┘
547 [second_countable_topology γ] [has_zero γ]
id └───────────────────────┘ └──────┘
src └───────────────────────┘ └──────┘
typ └───────────────────────┘ └──────┘
doc └───────────────────────┘
548
549 /-- Positive part of an `ae_eq_fun`. -/
550 def pos_part (f : α →ₘ γ) : α →ₘ γ :=
id ┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘
typ ┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘
551 comp₂ max (measurable.max (measurable.fst measurable_id) (measurable.snd measurable_id)) f 0
id └───┘ └─┘ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘ ┴
src └───┘ └─┘ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘
typ └───┘ └─┘ └────────────┘ └────────────┘ └───────────┘ └────────────┘ └───────────┘ ┴
doc └───┘
552
553 lemma pos_part_to_fun (f : α →ₘ γ) : ∀ₘ a, (pos_part f).to_fun a = max (f.to_fun a) (0:γ) :=
id ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴└─────┘ ┴ ┴
src └┘ └┘ ┴ └──────┘ └────┘ ┴ └─┘ └─────┘
typ ┴ └┘ ┴ └┘ ┴┴ └──────┘ ┴ └────┘ ┴ ┴ └─┘ ┴└─────┘ ┴ ┴
doc └┘ └┘ ┴ └──────┘ └────┘ └─────┘
554 begin
st └─────
555 filter_upwards [comp₂_to_fun max (measurable.max (measurable.fst measurable_id)
id └──────────┘ └─┘ └────────────┘ └────────────┘
src └──────────────┘└──────────┘┴└─┘┴ └────────────┘┴ └────────────┘┴ └─
typ └──────────────┘└──────────┘┴└─┘┴ └────────────┘┴ └────────────┘┴ └─
doc └──────────────┘ ┴ ┴ ┴ ┴ └─
txt └──────────────┘ ┴ ┴ ┴ ┴ └─
par └──────────────┘ ┴ ┴ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────────────────
556 (measurable.snd measurable_id)) f 0, @ae_eq_fun.zero_to_fun α γ],
id └────────────┘ └───────────┘ ┴ └───────────────────┘ ┴ ┴
src ───┘ └────────────┘┴└───────────┘└─┘ └──┘ └───────────────────┘┴ ┴ ┴
typ ───┘ └────────────┘┴└───────────┘└─┘┴└──┘ └───────────────────┘┴┴┴┴┴
doc ───┘ ┴ └─┘ └──┘ ┴ ┴ ┴
txt ───┘ ┴ └─┘ └──┘ ┴ ┴ ┴
par ───┘ ┴ └─┘ └──┘ ┴ ┴ ┴
pid ───┘ ┴ └─┘ └──┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
557 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
558 assume a h₁ h₂,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
559 rw [pos_part, h₁, h₂]
id └──────┘ └┘ └┘
src └──┘└──────┘└┘ └┘ └┘
typ └──┘└──────┘└┘└┘└┘└┘└┘
doc └──┘└──────┘└┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ─────────────┘└──┘└──┘┴┴
560 end
st └─┘
561
562 end pos_part
563
564 end ae_eq_fun
565
566 end measure_theory